only k(v):B sends [tg,f(s;v)] : T on l
== (e:E. loc(e) = source(l)  kind(e) = k  (e':E. kind(e') = rcv(l,tg) & sender(e') = e))
== & (e':E.
== & (kind(e') = rcv(l,tg)
== & ( kind(sender(e')) = k
== & ( & valtype(sender(e'))  B
== & ( & valtype(e')  T
== & ( & val(e') = f((state when sender(e'));val(sender(e')))
== & ( & & (e'':E. kind(e'') = rcv(l,tg)  sender(e'') = sender(e')  e'' = e')) 

latex

---

clarification:

es-only-sender(es; k; B; l; tg; T; s,v.f(s;v))
== (e:es-E(es).
== (es-loc(es; e) = source(l)  Id
== ( es-kind(es; e) = k  Knd
== ( (e':es-E(es). es-kind(es; e') = rcv(l,tg)  Knd & es-sender(es; e') = e  es-E(es)))
== & (e':es-E(es).
== & (es-kind(es; e') = rcv(l,tg)  Knd
== & ( es-kind(es; es-sender(es; e')) = k  Knd
== & ( & es-valtype(es; es-sender(es; e'))  B
== & ( & es-valtype(es; e')  T
== & ( & es-val(es; e') = f(es-state-when(es;es-sender(es; e'));es-val(es; es-sender(es; e')))  T
== & ( & & (e'':es-E(es).
== & ( & & (es-kind(es; e'') = rcv(l,tg)  Knd
== & ( & & ( es-sender(es; e'') = es-sender(es; e')  es-E(es)
== & ( & & ( e'' = e'  es-E(es))) 

latex

Definitions	Id, loc(e), source(l), x:A. B(x), A & B, valtype(e), P & Q, (state when e), val(e), x:A. B(x), Knd, kind(e), rcv(l,tg), P  Q, sender(e), E
FDL editor aliases	es-only-sender